|
In theoretical computer science a simulation preorder is a relation between state transition systems associating systems which behave in the same way in the sense that one system ''simulates'' the other. Intuitively, a system simulates another system if it can match all of its moves. The basic definition relates states within one transition system, but this is easily adapted to relate two separate transition systems by building a system consisting of the disjoint union of the corresponding components. ==Formal definition== Given a labelled state transition system (S, Λ, →), a ''simulation'' relation is a binary relation R over S (i.e. R ⊆ S × S) such that for every pair of elements (p,q) ∈ R, for all α ∈ Λ, and for all p' ∈ S, : implies that there is a q' ∈ S such that : and (p',q') ∈ R. Equivalently, in terms of relational composition: : Given two states p and q in S, q ''simulates'' p, written p ≤ q if there is a simulation R such that (p, q) ∈ R. The relation ≤ is a preorder, and is usually called the ''simulation preorder''. It is the largest simulation relation over a given transition system. Two states ''p'' and ''q'' are said to be ''similar'', written p ≤≥ q, if ''p'' simulates ''q'' and ''q'' simulates ''p''. Similarity is an equivalence relation, but it is coarser than bisimilarity. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Simulation preorder」の詳細全文を読む スポンサード リンク
|